package edu.lambdateacher.reductions;

import edu.lambdateacher.PropertiesManager;
import edu.lambdateacher.awt.MessageDialog;
import edu.lambdateacher.expressions.Abstraction;
import edu.lambdateacher.expressions.Application;
import edu.lambdateacher.expressions.Expression;
import edu.lambdateacher.expressions.HalfApplNumOp;
import edu.lambdateacher.expressions.Numbers;
import edu.lambdateacher.expressions.NumericalOperator;
import edu.lambdateacher.expressions.NumericalOperatorType;

public class BetaReduction {
	public static boolean betaAllowed(Expression thefunc, Expression thearg, Expression arg) {
		// keep skipping bindings until the function part is reached

		// first check if the func is a numerical
		// operator or half applied numerical operator.
		if ((thefunc instanceof NumericalOperator) || (thefunc instanceof HalfApplNumOp)) {
			// if the function is a number, return true..
			if (thearg instanceof Numbers) {
				return true;
			} else {
				return false; // otherwise, return false.
			}
		}

		// if func isn't abstraction, can't beta reduce.
		if (!(thefunc instanceof Abstraction))
			return false;

		// if the func has a null bound variable, can't beta reduce.
		if (((Abstraction) thefunc).getBoundVar() == null)
			return false;

		// if arg is null, can't beta reduce.
		if (arg == null)
			return false;

		// if we've survived to here, we can beta reduce.
		return true;
	}
	
	/**
	 * beta_reduce subs arg into the body of function, and returns the new body
	 * if beta_allowed. It also sets parentmodified to true, because beta
	 * reducing should wipe out all upper bindings.
	 */
	// TODO: Implement Strategy pattern here
	public static Expression betaReduce(Application application) {
		
		Expression toreturn = application;
		
		// is beta reduction allowed?
		boolean beta_allow = toreturn.betaAllowed();
		// does this beta reduction involve an Abstraction
		boolean involveabs = false;
		// does this beta reduction involve a NumericalOperator
		boolean involvenumop = false;
		// does this beta reduction involve a HalfApplNumOp
		boolean involvehalfapp = false;
		// a string which represents the function
		String funcstr = null;
		// a string which represents the arg
		String argstr = null;
		// a string which represents the bound variable
		String bvar = null;
		String thisstr = toreturn.stringRepresentation(false);

		if (beta_allow == true) {
			// keep skipping bindings for the function and arg
			Expression thefunc = application.getFuncSkipBindings();
			Expression thearg = application.getArgSkipBindings();

			// make copies of function and arg strings
			if (PropertiesManager.expdlogon) {
				funcstr = thefunc.stringRepresentation(false);
				argstr = thearg.stringRepresentation(false);
			}

			// first check for a numerical operator or
			// half applied numerical operator.
			if (thefunc instanceof NumericalOperator) {
				involvenumop = true;

				// set the return expression
				toreturn = new HalfApplNumOp((NumericalOperator) thefunc, (Numbers) thearg);
			} else if (thefunc instanceof HalfApplNumOp) {
				toreturn = ((HalfApplNumOp)thefunc).betaReduce(application);
			} else if (thefunc instanceof Abstraction) {
				toreturn = ((Abstraction)thefunc).betaReduce(application);
			}
			// set parentmodified to true, as all upper bindings
			// are modified.
			toreturn.setParentModified(true);
		}

		// now bring up the explanation dialog
		// TODO use a properties file to store the information inside the strings
		if (PropertiesManager.expdlogon) {
			String message = "";
			if (!beta_allow) {
				message = message + "The Lambda Application:\n\n" + thisstr + "\n\n";
				message = message + "is not reducable (can't be beta reduced).\n";
				message = message + "This is because the function part of the application is not ";
				message = message + "a valid Lambda Abstraction (\\x.M), the argument part of the ";
				message = message + "application is invalid, or the function and argument do ";
				message = message + "not match.";
			} else {
				message = message + "The expression:\n\n" + thisstr + "\n\n";
				message = message + "is being reduced.\n";
				if (involveabs == true) {
					message = message + "This is a BETA reduction, because the application is of ";
					message = message + "the form (Abstraction) (Arg).\n";
					message = message + "A BETA reduction can be seen as a function substitution, ";
					message = message + "where :\n\n";
					message = message + funcstr + "\n\nis the function, and :\n\n" + argstr + "\n\n";
					message = message + "is the argument.\n";
					message = message + "The argument expression is substituted for the bound variable (";
					message = message + bvar + ") in the body of the function expression, giving a result of:\n\n";
					message = message + toreturn.stringRepresentation(false);
				} else if (involvenumop == true) {
					message = message + "This is a BETA reduction, because the application is of ";
					message = message + "the form (Numerical Operator) (Number).\n";
					message = message + "The Numerical Operator " + "\"" + funcstr + "\"" + " is applied to the Number ";
					message = message + "\"" + argstr + "\"" + " to produce ";
					message = message + "a new function which consists of the Numerical Operator applied ";
					message = message + "to one argument.\n";
					message = message + "This new function is: \n";
					message = message + toreturn.stringRepresentation(false);
				} else if (involvehalfapp == true) {
					message = message + "This is a BETA reduction, because the application is of ";
					message = message + "the form (Half Applied Numerical Operator) (Number).\n";
					message = message + "The Half Applied Numerical Operator " + "\"" + funcstr + "\"" + " is applied to the Number ";
					message = message + "\"" + argstr + "\"" + " to produce ";
					message = message + "a result which is a number " + "\"" + toreturn.stringRepresentation(false) + "\".";
				}
			}
		}

		return toreturn;
	}
	
}
